/*
 * =====================================================================================
 *
 *       Filename:  demo_bdd.c
 *
 *    Description:  A demo program to show how operations on BDD are
 *    implemented.
 *
 *        Version:  1.0
 *        Created:  Thursday 18 August 2011 01:15:29  IST
 *       Revision:  none
 *       Compiler:  gcc
 *
 *         Author:  Dilawar Singh (Graduate Student, EE IITB), dilawar@ee.iitb.ac.in
 *      Institute:  IIT Bombay
 *
 * =====================================================================================
 */


#include	<stdio.h>
#include	<stdlib.h>
#include	<string.h> /*  for length function. */
#define addr_(a) (addr)(size_t)(a)

typedef unsigned int addr;
int totalNodes = 0; /* this many nodes are currently in use. */

typedef struct node
{
    char *v; /* variable name, We may not use it. It's not nartural to compare two character. */
    addr lo;
    addr hi;
    unsigned int index;
    int vRef; /*  reference count minus 1 */
} bddNode;

int i;

void printNode(bddNode*);
bddNode* constructBdd(char* fVar[], char* var[], char* binOp); 

bddNode mem[100];

/*  
 *  Since sink nodes  never change, let's define and put them in 'mem' at bottom. There,
 *  they will rest in peace all the time.
 */
bddNode* sink0; 
bddNode* sink1; 

int main()
{
    /*  Let's define variables with ordering. There are algorithms available to
     *  find a suitable ordering such that BDD size is minimum. For now, we
     *  assume that ordering is know to us */

    /*  for simplicity sake, char 1 means x_1 and so on. */
    char *var[] = {"1", "2", "3"}; /*  Note that these are char and not numbers. */
    
    /*  Now we should have some binary operations. What is a use of BDDs if we
     *  can not compose them. */
    char *binOp[] = {"&", "|", "^", "$", "#"}; /* I am not using all of them.  */

    /*  now we need to construct some bdd so that we can have some fun! Ideally,
     *  there should be a function to which we can pass a boolean function and
     *  presto, we get a bdd. Why don't you do that and I hardcode two BDD's.*/

    /*  I am hardcoding two bdds, bdd1 and bdd2. Later we will combine them
     *  using a binary operation and produce a new BDD. 
     *
     * let bdd1 = x_1 | x_3, read x_1 'or' x_3.
     * NOTE : Sink nods are labelled as 000 (0) and 011. DO NOT CONFUSE THEM
     * WITH OTHER NODE LEVELS which are variable names.
     *
     *              1
     *             / \
     *           LO   \
     *           /     HI
     *          3       \
     *        /  \      011
     *       LO   HI
     *      /      \
     *    000      011
     */ 

    /*  initialize sink nodes */
    sink0 = mem;
    sink1 = mem + 1;
    totalNodes += 2;
    sink0->v = "0";
    sink0->lo = 0;
    sink0->hi = 0;

    sink1->v = "0";
    sink1->lo = 1;
    sink1->hi = 1;

    /*  let's construct bdd1 */
    char* var1[] = {"1", "3"};
    bddNode* bdd1 = constructBdd(var1, var, "&"); 

    /*  and now bdd2 which is x_2 xor x_3 
     *            
     *            2
     *         /    \
     *        LO      HI
     *       /         \
     *      3           3
     *     / \         / \
     *    LO  HI     HI  LO
     *     |    \   /    /
     *     |     \/     /
     *      \   /  \   /
     *       000    011
     *   
     */
    char* var2[] = {"2", "3"};
    bddNode* bdd2 = constructBdd(var2, var, "^"); 
    return 0;
}

void printNode(bddNode* p)
{
    printf("Node : ");
    printf(" (%d, %x, %x)\n", p->index, addr_(p->lo), addr_(p->hi));
}

bddNode* constructBdd(char* fVar[], char* var[], char* binOp)
{
    if (strncmp(binOp, "&", 1) == 0)
    {
        printf("Building a BDD with AND operation\n");
        printf("Binary operation is %s\n", binOp); 
        bddNode* r = mem + totalNodes + 1; totalNodes++;
        bddNode* rl = mem + totalNodes + 1; totalNodes++;
        r->index = (int) (fVar[0] - 48) ;
        r->lo = addr_(rl);
        r->hi = addr_(sink1);
        rl->index = (int) (fVar[1] - 48);
        rl->lo = addr_(sink0);
        rl->hi = addr_(sink1);
        printNode(r);
        return r;
    }
    else
    {
        printf("Write routine to implement other binary opeation here!\n");
        return NULL;
    }
}

